/**
 * Developed by PuzzleDev s.n.c.
 * 2012 all rights reserved.
 * www.puzzledev.com
 */
package it.polimi.nuzot.core

import org.junit._
import Assert._
import it.polimi.nuzot.ltl.LTLInterpreter
import it.polimi.nuzot.shell.ShellParser
import it.polimi.nuzot.shell.ShellInterpreter
import it.polimi.nuzot.smt.TypeChecker
import it.polimi.nuzot.smt.grammar.Script
import it.polimi.nuzot.Z3.Z3Interpreter


/**
 * @author Michele Sama (m.sama@puzzledev.com)
 *
 */
class NuZotIntegrationTestCase {

    /**
     * Assert the correct execution of a script
     * in a working environment.
     */
    def assertExecution(input: String, expected: Boolean) = {
        val parser = new ShellParser()
        val inputScript = parser.parseAll(
		                parser.script, input)
		                .getOrElse(null)
		
		// Recreates a complete execution stack
		val z3 = new Z3Interpreter()
        val typeChecker = new TypeChecker()
        typeChecker.next(z3)
		val ltl = new LTLInterpreter()
    	ltl.next(typeChecker)
    	ltl.temporalExt = 5
		val shell = new ShellInterpreter()
        shell.next(ltl)
    			
        shell.doVisitPreconditions(Script(List())) ++ 
        		shell.doVisit(inputScript)
        assertEquals(input, shell.precomputed.toString())
        assertEquals(input, ltl.precomputed.toString())
        //assertEquals(expected, z3.precomputed.toString())
        assertEquals(expected, z3.checkSat())
    }
    
    @Test
    def testDoubleNext() = {
        val input = 
            	"(declare-tfun x () Bool)\n" +
        		"(assert (next (next x)))"
        assertExecution(input, true)
    }
    
    @Test
    def testNextUntil() = {
        val input = 
            	"(declare-tfun x () Bool)\n" +
            	"(declare-tfun y () Bool)\n" +
        		"(assert (next (until x y)))"
        assertExecution(input, true)
    }
    
    @Test
    def testUntilGt() = {
        val input = 
            	"(declare-tfun x () Int)\n" +
            	"(declare-tfun y () Int)\n" +
            	"(declare-tfun z () Bool)\n" +
        		"(assert (until (> x y) z))"
        assertExecution(input, true)
    }
}